% -*- TeX-PDF-mode: t; TeX-master: "proposal"; -*-

\documentclass{llncs}

\usepackage{xspace}
\usepackage{url}
\usepackage{cite}
\usepackage{hyperref}

\newcommand{\biojpf}{{\sc BioJPF}\xspace}
\newcommand{\jpf}{{\sc JPF}\xspace}
\newcommand{\gsoc}{{\sc GSOC}\xspace}
\begin{document}

% The JPF application template has the following items/questions:

% 1. Project title

% 2. Project description

% 3. What is the development methodology you propose to use for the
% project? Please include information on possible deliverables and the
% tentative schedule.

% 4. What are the goals that you hope to accomplish in your project?

% 5. Tell us about yourself (university, department, year). What are
% your qualifications, interests, and expectations? Have you worked on
% an open-source project in that past, whether through JPF, Google
% Summer of Code, or otherwise?

% 6. What is your availability this summer? Do you have other
% commitments?

% 7. Briefly describe any discussions you have had with JPF mentors
% about your project. (We encourage that you contact the mentors and
% discuss ideas with them before submitting an application)


\title{Analysis of biological models in Symbolic PathFinder}
\subtitle{\small Project Proposal for the Google Summer of Code 2013}

\author{Jos\'e Miguel Rojas}
\institute{Technical University of Madrid, Spain\\
josemiguel.rojas@upm.es $|$ jmrs84@gmail.com \\
}
\maketitle

\begin{abstract}
  This project aims at modelling biological systems in a Statechart
  dialect of Java and applying model checking techniques to verify
  properties of interest such as stabilization or consistency with
  respect to a set of laboratory experimental observations.  In
  particular, the project will focus on the C. elegans roundworm,
  which is a model organism extensively used in biological research
  because of its simplicity and tractability.  The project will
  provide implementations for the particular composition operator and
  abstractions used in these models.  The tool to be developed should
  be simple, intuitive and user-friendly in order to actually be
  useful for biological researchers.
\end{abstract}

\section{Project Description}

Computational biology has gained a lot of interest as a means to
better understanding the behavior of complex biological systems.  It
provides the biological research community with tools and
methodologies to interpret and analyze large amounts of data,
accurately create and simulate models of biological systems (e.g., the
human brain), and gain new insights and make predictions about how a
biological system will react under different environments, etc.
Executable biology is a research line that focuses on the
design of executable computer algorithms that mimic biological
phenomena \cite{Fisher2007}.  Statecharts are an instance of
computational formalisms that can be used to model complex biological
systems \cite{Harel1987,Harel03formalmodeling,Kam01theimmune}.

This project aims at extending the application domain of Java
PathFinder (\jpf) to complex biological systems modeled with
statecharts formalisms.  The development of the project will begin
with a study of the literature in the field and the identification of
properties of biological systems that may be amenable for automated
formal verification via model checking.  In particular, for the
C. elegans organism, stabilization and consistency seem to be checkable
properties.  Stabilization determines where does a system end up after
a series of perturbations such as introduction of drugs or changes in
its genetic information.  Consistency must be checked against a set of
laboratory experimental observations and tells whether the
experimental observations correspond with the executable model
under analysis.

The functional requirement of the developed tool is simple. It should
take as input a statechart model in some suitable format (e.g., XML),
perform (symbolic) model checking on it and give a result with respect
to a specified property. As for non-functional requirements, in order
to be useful for the biological research community, the tool should be
flexible, intuitive and user-friendly.  An optional additional
implementation goal of this project is to incorporate a visual
interface to model biological systems.

\section{Main Objective}\label{sec:goals}
%\input{goals}

% 4. What are the goals that you hope to accomplish in your project?

The goal of this project is to design and implement a framework
based on \jpf for the analysis and verification of the C. elegans
model organism represented with statecharts formalisms.

\section{Development Methodology}
%\input{method}

% 3. What is the development methodology you propose to use for the
% project? Please include information on possible deliverables and the
% tentative schedule.

I propose to follow an agile software development methodology.  In an
agile methodology a working software is preferred over thorough
documentation. Interaction of the team members (me and the mentors)
and collaboration with the users are valued. Moreover, an agile
methodology favors flexibility and responding to changes over
following a rigorous planning.  In this spirit, three deliverables are
required and will be regularly updated during the project span: the
code itself, a set of case studies and a technical report.
  
The contact with the mentors will be permanent by email. Weekly
conference calls will help keep the focus, evaluate progress and
planning ahead.


\subsection{Timeline}

% 7. Briefly describe any discussions you have had with JPF mentors
% about your project. (We encourage that you contact the mentors and
% discuss ideas with them before submitting an application)

This project will be my primary activity during the period of the
\gsoc program.  The following is the tentative schedule for the project span:

~\\
\noindent\emph{June 17. Project starts}\\
\emph{Week 1}. Systematic Literature Review.\\
\emph{Weeks 2--3}. Develop meaningful case studies and define properties of
  interest to verify in C. elegans models.\\
\emph{Weeks 4--7}. Design and implement the modelling of C. elegans as
  a statechart dialect of Java. This includes composition operator and
  abstractions.\\
\emph{August 2. mid-term evaluation deadline}\\
\emph{Weeks 8--11}. Design and implement integration as extension of
  \jpf .\\
\emph{Weeks 12--14}. Validate implementation against case studies.\\
\emph{September 16. Suggested 'pencils down' date}\\
\emph{Week 15}. Write tests, scrub and optimize code and improve
  documentation.\\
\noindent\emph{September 23. Firm 'pencils down' date}

~\\
Finally, if time allows, an initial version of a research paper will
be written by the final evaluation deadline.

\section{Biographical Information}\label{sec:background}

% 5. Tell us about yourself (university, department, year). What are
% your qualifications, interests, and expectations? Have you worked on
% an open-source project in that past, whether through JPF, Google
% Summer of Code, or otherwise?

I am a PhD student at the Department of Languages, Systems and
Software Engineering of the Technical University of Madrid, under the
supervision of Elvira Albert and Miguel G\'omez-Zamalloa.  I have been
involved in several open-source projects. Currently I am core
contributor to the PET System, a partial evaluation-based test case
generation tool (\url{http://costa.ls.fi.upm.es/pet}). I have also
contributed to the COSTA System, a cost and termination analysis tool
(\url{http://costa.ls.fi.upm.es/costa}), and developed some
open-source research prototype tools for program transformation and
simulation of bio-inspired computational models.

\paragraph{Experience with \jpf.}

In the fall of 2013, I was a visitor research student at NASA Ames
under the supervision of Corina P\u{a}s\u{a}reanu. I worked on
Symbolic PathFinder, a symbolic execution extension of \jpf.  My work
consisted on developing a compositional approach to symbolic execution
based on program specialization.  A paper reporting preliminary
results of this work was accepted and presented at the BYTECODE'13
workshop (ETAPS'13 satellite event) \cite{RojasP13-short} and an
invitation to submit an extended journal version of the paper was
received.

\paragraph{Experience with biological models.}

As a master student, I did some work on the design and implementation
of Java simulators for bio(DNA)-inspired computational models
\cite{delRosalRNCO09,RojasCO10,NavarreteCAOR11}.  Namely, I worked
with Networks of Evolutionary Processors (NEPs) and Splicing Systems.
The former are computational devices inspired on cell biology. Each
node in a NEP represents a cell, working in parallel with the rest of
cells in a cell population. Each cell has genetic information encoded
in DNA sequences which evolve by local evolutionary events (called
point mutations: insertion, deletion or substitution of DNA
sub-sequences). Information flows between nodes in the system by means
of input and output filters between interconnected nodes. In my
previous work, we used this formalism to encode complex problems and
automatically solve them. In turn, Splicing Systems are computational
devices that model the DNA recombination operation and have been
proven very powerful as language generators, which was the context in
which we used them.

\section{Related Tools} 

Polyglot \cite{BalasubramanianPKL13} is a tool integrated in \jpf
which is relevant to this project.  It performs systematic analysis
and test-case generation of systems integrated from components built
using multiple Statechart formalisms.  Statechart models are
translated into a common Java representation with pluggable semantics
for diﬀerent Statechart variants.  Bio Model Analyzer (BMA)
\cite{BenqueBCCFIPTV12} is a modelling and analysis tool for
biological systems.  BMA is a good example of how a tool can be
presented to biologists with no (or very basic) background in
programming languages or formal methods. BMA implements techniques
based on formal methods that were developed for the specification and
verification of properties in concurrent software systems and relies
on them to analyze biological systems and establish cellular
stabilization.  Other related tools are surveyed at
\url{http://sbml.org/SBML_Software_Guide}.


%\section*{References}
\bibliographystyle{plain}
%\bibliographystyle{elsarticle-num}
\bibliography{project.bib}

\end{document}
